The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0, x2) → x2
drop#2(S(0), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0, x2) → Nil
take#2(S(0), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0) → 0
halve#1(S(0)) → S(0)
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0, x16) → True
leq#2(S(x20), 0) → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
take#2, drop#2, merge#2, leq#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(6) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
take#2, drop#2, merge#2, leq#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(7) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol take#2.

(8) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
drop#2, merge#2, leq#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol drop#2.

(10) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
leq#2, merge#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol leq#2.

(12) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
merge#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
halve#1 < map#2
length#1 < map#2

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol merge#2.

(14) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
halve#1, map#2, length#1

They will be analysed ascendingly in the following order:
halve#1 < map#2
length#1 < map#2

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol halve#1.

(16) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
length#1, map#2

They will be analysed ascendingly in the following order:
length#1 < map#2

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol length#1.

(18) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
map#2

(19) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11), rt ∈ Ω(1 + n848₁₁)

Induction Base:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0)) →_R^Ω(1)
Nil

Induction Step:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(n848_11, 1))) →_R^Ω(1)
Cons(dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11))) →_R^Ω(1)
Cons(Nil, map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11))) →_IH
Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(c849_11))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(20) Complex Obligation (BEST)

(21) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Lemmas:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11), rt ∈ Ω(1 + n848₁₁)

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

No more defined symbols left to analyse.

(22) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11), rt ∈ Ω(1 + n848₁₁)

(23) BOUNDS(n^1, INF)

(24) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Lemmas:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11), rt ∈ Ω(1 + n848₁₁)

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

No more defined symbols left to analyse.

(25) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n848_11), rt ∈ Ω(1 + n848₁₁)

(26) BOUNDS(n^1, INF)